#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "klee_change_macros.h"
#include "klee_change_functions.h"
int lib(int x) {
  if (x > klee_change(10,11))
    return 11;
  else
    return klee_change(x,x-1);
}

int client(int x) {
  if (x < -100 || x > 100) {
    return x;
  }
  if (x > lib(x))
    return x;
  else
    return lib(x);
}

int main(int argc, char *argv[]) {
  int x= argv[1][0] - '0';
  return client(x);
}
